consensus.4.jani:model: info: consensus.4 is an MDP model and will be simulated as an MDP.
consensus.4.jani:variables[6]: info: Expanding variable "pc1" into 4 locations in automaton "process1".
consensus.4.jani:variables[8]: info: Expanding variable "pc2" into 4 locations in automaton "process2".
consensus.4.jani:variables[10]: info: Expanding variable "pc3" into 4 locations in automaton "process3".
consensus.4.jani:variables[12]: info: Expanding variable "pc4" into 4 locations in automaton "process4".
consensus.4.jani: info: Using default value of 0.95 for the confidence parameter.
Peak memory usage: 58 MB
Analysis results for consensus.4.jani
Experiment K=4
Status: Finished
Simulation time: 599.5 s
+ Property Property "disagree"
Estimated max. probability: 0.03031598052965927
Runs used (best scheduler): 606050
Total runs used: 2364050
Schedulers sampled: 1000
Best scheduler: 28866019
Run type: MDP
Status: Finished
+ Error bounds
Scheduler sampling: The result is a lower bound for the true max. probability.
Statement: Adaptive: P(error > εp̂) < δ
ε: 0.02
δ: 0.050000000000000044